Nuprl Lemma : p-fun-exp-add
11,40
postcript
pdf
T
:Type,
n
,
m
:
,
f
:(
T
(
T
+ Top)).
f
^
n
+
m
=
f
^
n
o
f
^
m
T
(
T
+ Top)
latex
ProofTree
Definitions
P
Q
,
False
,
A
,
A
B
,
,
{
x
:
A
|
B
(
x
)}
,
,
x
:
A
.
B
(
x
)
,
{
i
..
j
}
,
t
T
,
f
o
g
,
x
.
A
(
x
)
,
primrec(
n
;
b
;
c
)
,
#$n
,
P
Q
,
x
:
A
B
(
x
)
,
P
&
Q
,
P
Q
,
f
^
n
,
Type
,
p-id()
,
Top
,
left
+
right
,
x
:
A
B
(
x
)
,
s
=
t
Lemmas
p-fun-exp-compose
,
p-id
wf
,
primrec
add
,
primrec
wf
,
p-compose
wf
,
int
seg
wf
origin
T:Type, n, m:
, f:(T
(T + Top)). f^n+m = f^n o f^m 
T(T + Top)
T:Type, n, m:, f:(T(T + Top)). f^n+m = f^n o f^m T(T + Top)
Q
A
B
x:A. B(x)
} T
x.A(x)
Q
B(x) QB(x)